$\forall$${\it es}$:ES, $a$:Atom1, $e$:E, $i$:Id. $e$ sends $a$ to $i$ $\in$ Prop